k:Knd, f, g:Top. ((islocal(k)))  (kindcase(k; a.f(a); l,t.g(l,t) ) ~ g(lnk(k),tag(k))) 

latex

Definitions	x:A. B(x), P  Q, b, islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), lnk(k), tag(k), b, isl(x), if b then t else f fi , act(k), t.1, outl(x), t.2, tt, ff, True, outr(x), t  T, Knd, A, False, , locl(a)
Lemmas	not wf, false wf, top wf, true wf, Knd wf